package gov.nasa.jpf.symbc.modelcounter.sampler;

import java.util.HashMap;
import java.util.Map;
import java.util.Random;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.symbc.modelcounter.ModelCounter;
import gov.nasa.jpf.symbc.numeric.MinMax;

/**
 * A model counter that "counts" model by sampling that variable space.
 */
public abstract class Sampler extends ModelCounter {

	/**
	 * Number of samples to take to find enough viable samples.
	 */
	protected int sampleLimit = 100000;

	/**
	 * Number of viable samples to take to find the probability.
	 */
	protected int nrOfSamples = 10000;

	/**
	 * Seed for the (pseudo-)random number generator.
	 */
	protected long rngSeed = 20111016;

	/**
	 * The (pseudo-)random number generator for our samples.
	 */
	protected Random rng;

	/**
	 * The number of samples taken during the run.
	 */
	protected long sampleCount = 0;

	private Map<String, Integer> variableNumbering;

	/**
	 * Constructor for the sampler. The first step is to read settings from the
	 * given configuration.
	 * 
	 * @param config
	 *            a JPF configuration
	 */
	public Sampler(Config config) {
		super(config);
		long y = config.getLong("symbolic.prob_seed", Long.MAX_VALUE);
		if (y != Long.MAX_VALUE) {
			rngSeed = y;
		}

		int x = config.getInt("symbolic.prob_sample_limit", 0);
		if (x > 0) {
			sampleLimit = x;
		} /* else: we ignore non-positive settings */

		x = config.getInt("symbolic.prob_nr_of_samples", 0);
		if (x > 0) {
			nrOfSamples = x;
		} /* else: we ignore non-positive settings */

		System.out.println("symbolic.prob_seed=" + rngSeed);
		System.out.println("symbolic.prob_sample_limit=" + sampleLimit);
		System.out.println("symbolic.prob_nr_of_samples=" + nrOfSamples);

		rng = new Random(rngSeed);
		sampleCount = 0;
		variableNumbering = new HashMap<String, Integer>();
	}

	/**
	 * Generate and return a random integer value that lies within the bounds
	 * (inclusive). The function assumes that the minimum value is equal to or
	 * less than the maximum value.
	 * 
	 * @param min
	 *            the minimum value generated
	 * @param max
	 *            the maximum value generated
	 * @return a random integer in the range [{@code min}..{@code max}]
	 */
	public int getRandomInt(int min, int max) {
		return min + rng.nextInt(max - min + 1);
	}

	/**
	 * Generate and return a random integer value with which the current
	 * variable-value assignment can be extended.
	 * 
	 * @return a random integer
	 */
	public int getRandomInt() {
		return getRandomInt(MinMax.getVarMinInt(null), MinMax.getVarMaxInt(null));
	}

	/**
	 * Generate and return a random integer value that lies within the range of
	 * the given variable.
	 * 
	 * @param varname
	 *            the name of the variable
	 * @return a random integer valid for the known range of the variable
	 */
	public int getRandomInt(String varname) {
		if (varname.endsWith("_SYMINT")) {
			varname = varname.replaceAll("_[0-9][0-9]*_SYMINT", "");
		}
		return getRandomInt(MinMax.getVarMinInt(varname), MinMax.getVarMaxInt(varname));
	}

	/**
	 * Generate and return a random double value with which the current
	 * variable-value assignment can be extended.
	 * 
	 * @return a random double
	 */
	/**
	 * Generate and return a random real value that lies within the bounds
	 * (inclusive). The function assumes that the minimum value is equal to or
	 * less than the maximum value.
	 * 
	 * @param min
	 *            the minimum value generated
	 * @param max
	 *            the maximum value generated
	 * @return a random real in the range [{@code min}..{@code max}]
	 */
	public double getRandomDouble(double min, double max) {
		return min + rng.nextDouble() * (max - min);
	}

	/**
	 * Generate and return a random double value with which the current
	 * variable-value assignment can be extended.
	 * 
	 * @return a random double
	 */
	public double getRandomDouble() {
		return getRandomDouble(MinMax.getVarMinDouble(null), MinMax.getVarMaxDouble(null));
	}

	/**
	 * Generate and return a random real value that lies within the range of the
	 * given variable.
	 * 
	 * @param varname
	 *            the name of the variable
	 * @return a random real valid for the known range of the variable
	 */
	public double getRandomDouble(String varname) {
		if (varname.endsWith("_SYMINT")) {
			varname = varname.replaceAll("_[0-9][0-9]*_SYMINT", "");
		}
		return getRandomDouble(MinMax.getVarMinDouble(varname),
				MinMax.getVarMaxDouble(varname));
	}

	/*
	 * (non-Javadoc)
	 * 
	 * @see gov.nasa.jpf.symbc.modelcounter.ModelCounter#report()
	 */
	@Override
	public void report() {
		System.out.println("Total nr of samples = " + sampleCount);
	}

	/**
	 * Return the canonical number for the given variable name.
	 * 
	 * @param name the name of the variable
	 * @return the unique identifier (an integer) for the variable
	 */
	public int getVariableId(String name) {
		if (!variableNumbering.containsKey(name)) {
			int id = variableNumbering.size();
			variableNumbering.put(name, id);
			return id;
		} else {
			return variableNumbering.get(name);
		}
	}

}
